Termination w.r.t. Q proof of /tmp/tmpbtb9fa/thiemann05.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(u, v) → if1(isLeaf(u), isLeaf(v), u, v)
if1(b, true, u, v) → false
if1(b, false, u, v) → if2(b, u, v)
if2(true, u, v) → true
if2(false, u, v) → less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(u, v) → if1(isLeaf(u), isLeaf(v), u, v)
if1(b, true, u, v) → false
if1(b, false, u, v) → if2(b, u, v)
if2(true, u, v) → true
if2(false, u, v) → less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(u, v) → if1(isLeaf(u), isLeaf(v), u, v)
if1(b, true, u, v) → false
if1(b, false, u, v) → if2(b, u, v)
if2(true, u, v) → true
if2(false, u, v) → less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))

The set Q consists of the following terms:

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

IF2(false, u, v) → LEFT(u)
LESS_LEAVES(u, v) → ISLEAF(u)
LESS_LEAVES(u, v) → IF1(isLeaf(u), isLeaf(v), u, v)
IF2(false, u, v) → RIGHT(u)
IF2(false, u, v) → RIGHT(v)
CONCAT(cons(u, v), y) → CONCAT(v, y)
IF2(false, u, v) → LEFT(v)
IF2(false, u, v) → CONCAT(left(u), right(u))
LESS_LEAVES(u, v) → ISLEAF(v)
IF2(false, u, v) → CONCAT(left(v), right(v))
IF1(b, false, u, v) → IF2(b, u, v)
IF2(false, u, v) → LESS_LEAVES(concat(left(u), right(u)), concat(left(v), right(v)))

The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(u, v) → if1(isLeaf(u), isLeaf(v), u, v)
if1(b, true, u, v) → false
if1(b, false, u, v) → if2(b, u, v)
if2(true, u, v) → true
if2(false, u, v) → less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))

The set Q consists of the following terms:

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF2(false, u, v) → LEFT(u)
LESS_LEAVES(u, v) → ISLEAF(u)
LESS_LEAVES(u, v) → IF1(isLeaf(u), isLeaf(v), u, v)
IF2(false, u, v) → RIGHT(u)
IF2(false, u, v) → RIGHT(v)
CONCAT(cons(u, v), y) → CONCAT(v, y)
IF2(false, u, v) → LEFT(v)
IF2(false, u, v) → CONCAT(left(u), right(u))
LESS_LEAVES(u, v) → ISLEAF(v)
IF2(false, u, v) → CONCAT(left(v), right(v))
IF1(b, false, u, v) → IF2(b, u, v)
IF2(false, u, v) → LESS_LEAVES(concat(left(u), right(u)), concat(left(v), right(v)))

The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(u, v) → if1(isLeaf(u), isLeaf(v), u, v)
if1(b, true, u, v) → false
if1(b, false, u, v) → if2(b, u, v)
if2(true, u, v) → true
if2(false, u, v) → less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))

The set Q consists of the following terms:

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 8 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CONCAT(cons(u, v), y) → CONCAT(v, y)

The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(u, v) → if1(isLeaf(u), isLeaf(v), u, v)
if1(b, true, u, v) → false
if1(b, false, u, v) → if2(b, u, v)
if2(true, u, v) → true
if2(false, u, v) → less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))

The set Q consists of the following terms:

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CONCAT(cons(u, v), y) → CONCAT(v, y)

R is empty.
The set Q consists of the following terms:

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CONCAT(cons(u, v), y) → CONCAT(v, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

CONCAT(cons(u, v), y) → CONCAT(v, y)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

LESS_LEAVES(u, v) → IF1(isLeaf(u), isLeaf(v), u, v)
IF1(b, false, u, v) → IF2(b, u, v)
IF2(false, u, v) → LESS_LEAVES(concat(left(u), right(u)), concat(left(v), right(v)))

The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(u, v) → if1(isLeaf(u), isLeaf(v), u, v)
if1(b, true, u, v) → false
if1(b, false, u, v) → if2(b, u, v)
if2(true, u, v) → true
if2(false, u, v) → less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))

The set Q consists of the following terms:

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

LESS_LEAVES(u, v) → IF1(isLeaf(u), isLeaf(v), u, v)
IF1(b, false, u, v) → IF2(b, u, v)
IF2(false, u, v) → LESS_LEAVES(concat(left(u), right(u)), concat(left(v), right(v)))

The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))

The set Q consists of the following terms:

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

LESS_LEAVES(u, v) → IF1(isLeaf(u), isLeaf(v), u, v)
IF1(b, false, u, v) → IF2(b, u, v)
IF2(false, u, v) → LESS_LEAVES(concat(left(u), right(u)), concat(left(v), right(v)))

The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))

The set Q consists of the following terms:

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule LESS_LEAVES(u, v) → IF1(isLeaf(u), isLeaf(v), u, v) at position [1] we obtained the following new rules:

LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1))
LESS_LEAVES(y0, leaf) → IF1(isLeaf(y0), true, y0, leaf)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1))
IF1(b, false, u, v) → IF2(b, u, v)
IF2(false, u, v) → LESS_LEAVES(concat(left(u), right(u)), concat(left(v), right(v)))
LESS_LEAVES(y0, leaf) → IF1(isLeaf(y0), true, y0, leaf)

The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))

The set Q consists of the following terms:

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1))
IF1(b, false, u, v) → IF2(b, u, v)
IF2(false, u, v) → LESS_LEAVES(concat(left(u), right(u)), concat(left(v), right(v)))

The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))

The set Q consists of the following terms:

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule IF2(false, u, v) → LESS_LEAVES(concat(left(u), right(u)), concat(left(v), right(v))) at position [1] we obtained the following new rules:

IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, right(cons(x0, x1))))
IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(left(cons(x0, x1)), x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, right(cons(x0, x1))))
IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(left(cons(x0, x1)), x1))
LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1))
IF1(b, false, u, v) → IF2(b, u, v)

The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))

The set Q consists of the following terms:

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, right(cons(x0, x1)))) at position [1,1] we obtained the following new rules:

IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(left(cons(x0, x1)), x1))
IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, x1))
LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1))
IF1(b, false, u, v) → IF2(b, u, v)

The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))

The set Q consists of the following terms:

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(left(cons(x0, x1)), x1)) at position [1,0] we obtained the following new rules:

IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, x1))
LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1))
IF1(b, false, u, v) → IF2(b, u, v)

The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))

The set Q consists of the following terms:

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1))

The remaining pairs can at least be oriented weakly.

IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, x1))
IF1(b, false, u, v) → IF2(b, u, v)

Used ordering: Polynomial interpretation [25]:

POL(IF1(x₁, x₂, x₃, x₄)) = x₄
POL(IF2(x₁, x₂, x₃)) = x₃
POL(LESS_LEAVES(x₁, x₂)) = 1 + x₂
POL(concat(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 1 + x₁ + x₂
POL(false) = 0
POL(isLeaf(x₁)) = x₁
POL(leaf) = 1
POL(left(x₁)) = 0
POL(right(x₁)) = x₁
POL(true) = 1

The following usable rules [17] were oriented:

concat(cons(u, v), y) → cons(u, concat(v, y))
concat(leaf, y) → y

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, x1))
IF1(b, false, u, v) → IF2(b, u, v)

The TRS R consists of the following rules:

isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))

The set Q consists of the following terms:

isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.